Nuprl Lemma : w-after-lemma2
0,22
postcript
pdf
w
:World. FairFifo
(
e
:E,
x
:Id. state_after(
e
).
x
= (
x
after
e
)
vartype(loc(
e
);
x
))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
,
World
,
FairFifo
,
E
,
Id
,
state_after(
e
)
,
s
.
x
,
<
a
,
b
>
,
s
=
t
,
loc(
e
)
,
vartype(
i
;
x
)
Lemmas
Id
wf
,
w-E
wf
,
fair-fifo
wf
,
world
wf
,
w-after-lemma
,
subtype
rel
self
,
w-vartype
wf
,
w-loc
wf
origin